ds:x:Id fp Type, da:k:Knd fp Type, a:ecl(ds;da). [a]*  ecl(ds;da) 

latex

Definitions	x:A. B(x), ecl(ds;da), t  T, [a]*, x. t(x), x(s)
Lemmas	nat wf, decl-state wf, ma-valtype wf, bool wf, Knd wf, fpf wf, Id wf